$\forall$${\it ds}$:$x$:Id fp$\rightarrow$ Type, ${\it da}$:$k$:Knd fp$\rightarrow$ Type, $x$:ecl(${\it ds}$;${\it da}$).
\\[0ex]($\uparrow$eclbase?($x$)) $\Rightarrow$ (eclbase{-}test($x$) $\in$ State(${\it ds}$)$\rightarrow$Valtype(${\it da}$;eclbase{-}k($x$))$\rightarrow\mathbb{B}$)